
; Copyright (c) 2015 Microsoft Corporation
(set-option :pp.max-depth 100)
(declare-fun f (Int Int) Int)
(declare-fun g (Int) Int)
(declare-fun p (Int) Bool)
(push)
(assert (forall ((x Int) (y Int)) (=> (and (= x (f (f x x) (f x y))) 
                                           (= y (f x x)))
                                      (= x y))))
(apply (and-then (! simplify :elim-and true) der))
(pop)


(push)
(assert (forall ((x Int) (y Int)) (=> (= x (f x y)) (p x))))
(assert (forall ((x Int) (y Int)) (not (= x (f y x)))))
(apply (and-then (! simplify :elim-and true) der))
(pop)

(push)
(assert (forall ((x Int) (y Int)) (not (= x (f y y)))))
(apply (and-then (! simplify :elim-and true) der))
(pop)


(push)
(assert (forall ((x1 Int) (x2 Int) (x3 Int)) 
                (=> (and (= x1 (g 0)) (= x2 (f x1 x1)) (= x3 (f x2 (g x1))))
                    (p x3))))
(assert (forall ((x1 Int) (x2 Int) (x3 Int)) 
                (=> (and (= x1 (g 0)) (= x2 (f x1 x3)) (= x3 (f x2 (g x1))))
                    (p x3))))
(apply (and-then (! simplify :elim-and true) der))
(pop)

(push)
(assert (forall ((x1 Int) (x2 Int) (x3 Int)) 
                (=> (and (= x2 (f x1 x1)) (= x1 (g 0)) (= x3 (f x2 (g x1))))
                    (p x3))))
(apply (and-then (! simplify :elim-and true) der))
(pop)

(push)
(assert (forall ((x1 Int) (x2 Int) (x3 Int)) 
                (=> (and (= x2 (f x1 x1)) (= x3 (f x2 (g x1))) (= x1 (g 0)))
                    (p x3))))
(apply (and-then (! simplify :elim-and true) der))
(pop)

(push)
(assert (forall ((x1 Int) (x2 Int) (x3 Int)) 
                (=> (and (= x2 (ite (forall ((y Int)) (= (g y) x1)) 1 0)))
                    (p x2))))
(apply (and-then (! simplify :elim-and true) der))
(pop)
